Promela の if

構文

code:promela

if

:: ブロック1

:: ブロック2

…

:: ブロックn

fi

例

code:promela

if

:: n == 0 -> printf("n == 0\n");

:: n >= 0 -> printf("n >= 0\n");

:: else -> printf("n < 0\n");

fi

与えられた枝のうち、実行可能なもの (ブロックされないもの) を実行する。

そのような枝が複数個ある場合、ランダムに（というか非決定的に）一つの枝を選んで実行する。

イメージとしては UNIX の select っぽい感じ？